AssertLemma `equiv\_rel\_iff` []